Inference at * 2 
Iof proof for Lemma member-exists:



1. T : Type
2. L : T List
3. (L = [])
  x:T. (x  L) 

latex

 by ((BLemma `member_exists`) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	x:A. B(x), P  Q, x:AB(x), x:A. B(x), x:A  B(x)
Lemmas	member exists